#include <tinx/debug.h>
#include <tinx/printk.h>
#include <tinx/device.h>
#include <tinx/task.h>
#include <tinx/stdarg.h>
#include <tinx/vsprintf.h>

static char buf[1024];

void debugk(char *file, int line, char *fmt, ...)
{
    dev_t dev = device_find(DEV_FLAG_SERIAL, 1);
    if (dev == EOF)
        return;

    task_t *task = running_task();

    va_list args;
    va_start(args, fmt);

    int i = sprintf(buf, "[%s] [%d] [%s] ", file, line, task->name);
    device_write(dev, buf, i, 0, 0);

    i = vsprintf(buf, fmt, args);
    device_write(dev, buf, i, 0, 0);

    va_end(args);
}